awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T₁ T₂ : (T : Triplet f g) × ↥(Spec T.tensor)
⊢ T₁ = T₂ ↔
    ∃ (e :
      T₁.fst (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) = T₂.fst (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))),
      (Spec.map (Triplet.tensorCongr e).inv) (T₁.snd (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))) =
        T₂.snd (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))
have mp : T₁ = T₂ →
  ∃ (e :
    T₁.fst (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) = T₂.fst (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))),
    (Spec.map (Triplet.tensorCongr e).inv) (T₁.snd (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))) =
      T₂.snd (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T₁ T₂ : (T : Triplet f g) × ↥(Spec T.tensor)
mp :
  T₁ = T₂ →
    ∃ (e :
      T₁.fst (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) = T₂.fst (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))),
      (Spec.map (Triplet.tensorCongr e).inv) (T₁.snd (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))) =
        T₂.snd (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))
⊢ T₁ = T₂ ↔
    ∃ (e :
      T₁.fst (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) = T₂.fst (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))),
      (Spec.map (Triplet.tensorCongr e).inv) (T₁.snd (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))) =
        T₂.snd (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))
have mpr : (∃ (e :
    T₁.fst (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) = T₂.fst (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))),
    (Spec.map (Triplet.tensorCongr e).inv) (T₁.snd (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))) =
      T₂.snd (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))) →
  T₁ = T₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T₁ T₂ : (T : Triplet f g) × ↥(Spec T.tensor)
⊢ (∃ (e :
      T₁.fst (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) = T₂.fst (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))),
      (Spec.map (Triplet.tensorCongr e).inv) (T₁.snd (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))) =
        T₂.snd (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))) →
    T₁ = T₂
have mpr : ∀ (T : Triplet f g) (snd : ↥(Spec T.tensor)),
  (∃ (e :
      Sigma.fst (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))
          (Sigma.mk (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) T snd) =
        T₂.fst (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))),
      (Spec.map (Triplet.tensorCongr e).inv)
          (Sigma.snd (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))
            (Sigma.mk (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) T snd)) =
        T₂.snd (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))) →
    Sigma.mk (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) T snd = T₂
Tactic: obtain ⟨T, _⟩ := T₁
Cleared hypotheses: T₁
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T₂ : (T : Triplet f g) × ↥(Spec T.tensor)
T : Triplet f g
snd : ↥(Spec T.tensor)
⊢ (∃ (e :
      Sigma.fst (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))
          (Sigma.mk (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) T snd) =
        T₂.fst (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))),
      (Spec.map (Triplet.tensorCongr e).inv)
          (Sigma.snd (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))
            (Sigma.mk (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) T snd)) =
        T₂.snd (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))) →
    Sigma.mk (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) T snd = T₂
have mpr : ∀ (T' : Triplet f g) (snd_1 : ↥(Spec T'.tensor)),
  (∃ (e :
      Sigma.fst (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))
          (Sigma.mk (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) T snd) =
        Sigma.fst (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))
          (Sigma.mk (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) T' snd_1)),
      Eq (α :=
        ↥(Spec
            (Sigma.fst (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))
                (Sigma.mk (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) T' snd_1)).tensor))
        ((Spec.map (Triplet.tensorCongr e).inv)
            (Sigma.snd (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))
              (Sigma.mk (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) T snd)) :
          ↥(Spec
              (Sigma.fst (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))
                  (Sigma.mk (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) T' snd_1)).tensor))
        (Sigma.snd (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))
            (Sigma.mk (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) T' snd_1) :
          ↥(Spec
              (Sigma.fst (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))
                  (Sigma.mk (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) T' snd_1)).tensor))) →
    Eq (α := (T : Triplet f g) × ↥(Spec T.tensor)) (Sigma.mk (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) T snd)
      (Sigma.mk (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) T' snd_1)
Tactic: obtain ⟨T', _⟩ := T₂
Cleared hypotheses: T₂
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.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)
have 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))
Tactic: apply carrierEquiv_eq_iff.mpr
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (hypothesis)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ 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))
have this : 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 _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
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)) ⊥) ⊥
⊢ 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))
have h : ((Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫ Spec.map (ofPointTensor (T.SpecTensorTo p))) ≫
      Spec.map (Triplet.tensorCongr sorry).hom)
    ⊥ =
  p
Tactic: simp only [SpecOfPoint, Triplet.tensorCongr_inv, ← this, ← Scheme.Hom.comp_apply,
      ← Scheme.Hom.comp_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
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)
have refine : IsEmpty.{u + 1} ↥(pullback f g) → Disjoint (α := Set ↥S) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥Y) ⇑g)
Tactic: refine ⟨?_, Scheme.isEmpty_pullback f g⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
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)
have 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
Tactic: rw [Set.disjoint_iff_forall_ne]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ 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
have 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)
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↥X
y : ↥Y
e : Eq (α := ↥S) (f x : ↥S) (g y : ↥S)
⊢ Nonempty.{u + 1} ↥(pullback f g)
have obtain : ∀ (z : ↥(pullback f g)), Nonempty.{u + 1} ↥(pullback f g)
Tactic: obtain ⟨z, -⟩ := exists_preimage_pullback x y e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (hypothesis)
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} ↥(pullback f g)
have this : Nonempty.{u + 1} ↥S
Tactic: have : Nonempty S := .map f ‹_›
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
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
⊢ Nonempty.{u + 1} ↥(pullback f g)
have rw : ∃ (x : ↥S),
  Membership.mem (γ := Set ↥S) (Set.range (ι := ↥X) ⇑f) x ∧ Membership.mem (γ := Set ↥S) (Set.range (ι := ↥Y) ⇑g) x
Tactic: rw [← not_isEmpty_iff, AlgebraicGeometry.Scheme.isEmpty_pullback_iff, Set.not_disjoint_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ Eq (α := Set ↥X) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.fst f g))
    (Set.preimage (β := ↥S) (⇑f) (Set.range (ι := ↥Y) ⇑g))
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
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
have 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
Tactic: refine ⟨?_, fun ⟨y, hy⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
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
⊢ 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
have 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
Tactic: refine ⟨?_, fun ⟨y, hy⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
a : ↥(pullback f g)
⊢ Membership.mem (α := ↥X) (γ := Set ↥X) (Set.preimage (β := ↥S) (⇑f) (Set.range (ι := ↥Y) ⇑g))
    ((pullback.fst f g) a : ↥X)
have h : ∃ (y : ↥Y), Eq (α := ↥S) (g y : ↥S) ((pullback.snd f g ≫ g) a : ↥S)
Tactic: simp only [Set.mem_preimage, Set.mem_range, ← Scheme.Hom.comp_apply, pullback.condition]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↥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
have h : ∀ (a : ↥(pullback f g))
  (ha : (pullback.fst f g) a = (Triplet.mk' x y sorry).x ∧ (pullback.snd f g) a = (Triplet.mk' x y sorry).y),
  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)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↥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)
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)
⊢ Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.fst f g)) x
have h : (pullback.fst f g) a = x
Tactic: use a, ha.left
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ Eq (α := Set ↥Y) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.snd f g))
    (Set.preimage (β := ↥S) (⇑g) (Set.range (ι := ↥X) ⇑f))
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
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
have 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
Tactic: refine ⟨?_, fun ⟨y, hy⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
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
⊢ 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
have 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
Tactic: refine ⟨?_, fun ⟨y, hy⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
a : ↥(pullback f g)
⊢ Membership.mem (α := ↥Y) (γ := Set ↥Y) (Set.preimage (β := ↥S) (⇑g) (Set.range (ι := ↥X) ⇑f))
    ((pullback.snd f g) a : ↥Y)
have h : ∃ (y : ↥X), Eq (α := ↥S) (f y : ↥S) ((pullback.fst f g ≫ f) a : ↥S)
Tactic: simp only [Set.mem_preimage, Set.mem_range, ← Scheme.Hom.comp_apply, ← pullback.condition]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↥Y
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
have 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
Tactic: obtain ⟨a, ha⟩ := Triplet.exists_preimage (Triplet.mk' y x hy)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↥Y
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)
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)
⊢ Membership.mem (γ := Set ↥Y) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.snd f g)) x
have h : (pullback.snd f g) a = x
Tactic: use a, ha.right
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ Eq (α := Set ↥S) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.snd f g ≫ g))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
have rw : Eq (α := Set ↥S) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.fst f g ≫ f))
  (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
Tactic: rw [← pullback.condition, range_fst_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
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)
⊢ Eq (α := Set ↥S) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.snd f g ≫ g))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
have rw₁ : Eq (α := Set ↥S) (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g) (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
Tactic: rw [← pullback.condition, range_fst_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
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₃
⊢ 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₂))
have 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
Tactic: ext z
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
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')
⊢ 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
have 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
Tactic: constructor