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
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
⊢ 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.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
Tactic: constructor
-- 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₃
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'))
have 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'))
Tactic: constructor
-- 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₃
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'))
⊢ 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'))
have 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'))
Tactic: constructor
-- 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₃
t : ↥(pullback f g)
⊢ 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'))
have h : Eq (α := ↥X') (i₁ ((pullback.fst f g) t : ↥X) : ↥X')
  ((pullback.fst f' g') ((pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) t : ↥(pullback f' g')) : ↥X')
Tactic: use pullback.fst f g t
-- 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₃
t : ↥(pullback f g)
⊢ Eq (α := ↥X') (i₁ ((pullback.fst f g) t : ↥X) : ↥X')
    ((pullback.fst f' g') ((pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) t : ↥(pullback f' g')) : ↥X')
have h : Eq (α := ↥X') ((pullback.fst f g ≫ i₁) t : ↥X')
  ((CategoryStruct.comp (Y := pullback f' g') (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) (pullback.fst f' g')) t : ↥X')
Tactic: rw [← 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
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)
⊢ 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'))
have h : Eq (α := ↥Y') (i₂ ((pullback.snd f g) t : ↥Y) : ↥Y')
  ((pullback.snd f' g') ((pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) t : ↥(pullback f' g')) : ↥Y')
Tactic: use pullback.snd f g t
-- 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₃
t : ↥(pullback f g)
⊢ Eq (α := ↥Y') (i₂ ((pullback.snd f g) t : ↥Y) : ↥Y')
    ((pullback.snd f' g') ((pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) t : ↥(pullback f' g')) : ↥Y')
have h : Eq (α := ↥Y') ((pullback.snd f g ≫ i₂) t : ↥Y')
  ((CategoryStruct.comp (Y := pullback f' g') (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) (pullback.snd f' g')) t : ↥Y')
Tactic: rw [← 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
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')
x : ↥X
hx : Eq (α := ↥X') (i₁ x : ↥X') ((pullback.fst f' g') z : ↥X')
y : ↥Y
hy : Eq (α := ↥Y') (i₂ y : ↥Y') ((pullback.snd f' g') z : ↥Y')
T₁ : Triplet (X := pullback f' g') (pullback.fst f' g') i₁ := Triplet.mk' z x ⋯
⊢ Membership.mem (γ := Set ↥(pullback f' g'))
    (Set.range (ι := ↥(pullback f g)) ⇑(pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂)) z
have h : ∀ (w₁ : ↥(pullback (X := pullback f' g') (pullback.fst f' g') i₁))
  (hw₁ : (pullback.fst (pullback.fst f' g') i₁) w₁ = T₁.x ∧ (pullback.snd (pullback.fst f' g') i₁) w₁ = T₁.y),
  Membership.mem (γ := Set ↥(pullback f' g'))
    (Set.range (ι := ↥(pullback f g)) ⇑(pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂)) z
Tactic: obtain ⟨w₁, hw₁⟩ := T₁.exists_preimage
-- 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')
x : ↥X
hx : Eq (α := ↥X') (i₁ x : ↥X') ((pullback.fst f' g') z : ↥X')
y : ↥Y
hy : Eq (α := ↥Y') (i₂ y : ↥Y') ((pullback.snd f' g') z : ↥Y')
T₁ : Triplet (X := pullback f' g') (pullback.fst f' g') i₁ := Triplet.mk' z x ⋯
w₁ : ↥(pullback (X := pullback f' g') (pullback.fst f' g') i₁)
hw₁ : (pullback.fst (pullback.fst f' g') i₁) w₁ = T₁.x ∧ (pullback.snd (pullback.fst f' g') i₁) w₁ = T₁.y
T₂ : Triplet (X := pullback f' g') (pullback.snd f' g') i₂ := Triplet.mk' z y ⋯
⊢ Membership.mem (γ := Set ↥(pullback f' g'))
    (Set.range (ι := ↥(pullback f g)) ⇑(pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂)) z
have h : ∀ (w₂ : ↥(pullback (X := pullback f' g') (pullback.snd f' g') i₂))
  (hw₂ : (pullback.fst (pullback.snd f' g') i₂) w₂ = T₂.x ∧ (pullback.snd (pullback.snd f' g') i₂) w₂ = T₂.y),
  Membership.mem (γ := Set ↥(pullback f' g'))
    (Set.range (ι := ↥(pullback f g)) ⇑(pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂)) z
Tactic: obtain ⟨w₂, hw₂⟩ := T₂.exists_preimage
-- 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')
x : ↥X
hx : Eq (α := ↥X') (i₁ x : ↥X') ((pullback.fst f' g') z : ↥X')
y : ↥Y
hy : Eq (α := ↥Y') (i₂ y : ↥Y') ((pullback.snd f' g') z : ↥Y')
T₁ : Triplet (X := pullback f' g') (pullback.fst f' g') i₁ := Triplet.mk' z x ⋯
w₁ : ↥(pullback (X := pullback f' g') (pullback.fst f' g') i₁)
hw₁ : (pullback.fst (pullback.fst f' g') i₁) w₁ = T₁.x ∧ (pullback.snd (pullback.fst f' g') i₁) w₁ = T₁.y
T₂ : Triplet (X := pullback f' g') (pullback.snd f' g') i₂ := Triplet.mk' z y ⋯
w₂ : ↥(pullback (X := pullback f' g') (pullback.snd f' g') i₂)
hw₂ : (pullback.fst (pullback.snd f' g') i₂) w₂ = T₂.x ∧ (pullback.snd (pullback.snd f' g') i₂) w₂ = T₂.y
T : Triplet (X := pullback (X := pullback f' g') (pullback.fst f' g') i₁) (Y :=
  pullback (X := pullback f' g') (pullback.snd f' g') i₂) (pullback.fst (pullback.fst f' g') i₁)
  (pullback.fst (pullback.snd f' g') i₂) :=
  Triplet.mk' w₁ w₂ ⋯
⊢ Membership.mem (γ := Set ↥(pullback f' g'))
    (Set.range (ι := ↥(pullback f g)) ⇑(pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂)) z
have h : ∀
  (t :
    ↥(pullback (X := pullback (X := pullback f' g') (pullback.fst f' g') i₁) (Y :=
        pullback (X := pullback f' g') (pullback.snd f' g') i₂) (pullback.fst (pullback.fst f' g') i₁)
        (pullback.fst (pullback.snd f' g') i₂))),
  (pullback.fst (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂)) t = T.x →
    ∀ (ht₂ : (pullback.snd (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂)) t = T.y),
      Membership.mem (γ := Set ↥(pullback f' g'))
        (Set.range (ι := ↥(pullback f g)) ⇑(pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂)) z
Tactic: obtain ⟨t, _, ht₂⟩ := T.exists_preimage
-- 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')
x : ↥X
hx : Eq (α := ↥X') (i₁ x : ↥X') ((pullback.fst f' g') z : ↥X')
y : ↥Y
hy : Eq (α := ↥Y') (i₂ y : ↥Y') ((pullback.snd f' g') z : ↥Y')
T₁ : Triplet (X := pullback f' g') (pullback.fst f' g') i₁ := Triplet.mk' z x ⋯
w₁ : ↥(pullback (X := pullback f' g') (pullback.fst f' g') i₁)
hw₁ : (pullback.fst (pullback.fst f' g') i₁) w₁ = T₁.x ∧ (pullback.snd (pullback.fst f' g') i₁) w₁ = T₁.y
T₂ : Triplet (X := pullback f' g') (pullback.snd f' g') i₂ := Triplet.mk' z y ⋯
w₂ : ↥(pullback (X := pullback f' g') (pullback.snd f' g') i₂)
hw₂ : (pullback.fst (pullback.snd f' g') i₂) w₂ = T₂.x ∧ (pullback.snd (pullback.snd f' g') i₂) w₂ = T₂.y
T : Triplet (X := pullback (X := pullback f' g') (pullback.fst f' g') i₁) (Y :=
  pullback (X := pullback f' g') (pullback.snd f' g') i₂) (pullback.fst (pullback.fst f' g') i₁)
  (pullback.fst (pullback.snd f' g') i₂) :=
  Triplet.mk' w₁ w₂ ⋯
t :
  ↥(pullback (X := pullback (X := pullback f' g') (pullback.fst f' g') i₁) (Y :=
      pullback (X := pullback f' g') (pullback.snd f' g') i₂) (pullback.fst (pullback.fst f' g') i₁)
      (pullback.fst (pullback.snd f' g') i₂))
left : (pullback.fst (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂)) t = T.x
ht₂ : (pullback.snd (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂)) t = T.y
⊢ Membership.mem (γ := Set ↥(pullback f' g'))
    (Set.range (ι := ↥(pullback f g)) ⇑(pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂)) z
have h : (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) ((Iso.hom (pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂)) t : ↥(pullback f g)) = z
Tactic: use (pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).hom t
-- 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')
x : ↥X
hx : Eq (α := ↥X') (i₁ x : ↥X') ((pullback.fst f' g') z : ↥X')
y : ↥Y
hy : Eq (α := ↥Y') (i₂ y : ↥Y') ((pullback.snd f' g') z : ↥Y')
T₁ : Triplet (X := pullback f' g') (pullback.fst f' g') i₁ := Triplet.mk' z x ⋯
w₁ : ↥(pullback (X := pullback f' g') (pullback.fst f' g') i₁)
hw₁ : (pullback.fst (pullback.fst f' g') i₁) w₁ = T₁.x ∧ (pullback.snd (pullback.fst f' g') i₁) w₁ = T₁.y
T₂ : Triplet (X := pullback f' g') (pullback.snd f' g') i₂ := Triplet.mk' z y ⋯
w₂ : ↥(pullback (X := pullback f' g') (pullback.snd f' g') i₂)
hw₂ : (pullback.fst (pullback.snd f' g') i₂) w₂ = T₂.x ∧ (pullback.snd (pullback.snd f' g') i₂) w₂ = T₂.y
T : Triplet (X := pullback (X := pullback f' g') (pullback.fst f' g') i₁) (Y :=
  pullback (X := pullback f' g') (pullback.snd f' g') i₂) (pullback.fst (pullback.fst f' g') i₁)
  (pullback.fst (pullback.snd f' g') i₂) :=
  Triplet.mk' w₁ w₂ ⋯
t :
  ↥(pullback (X := pullback (X := pullback f' g') (pullback.fst f' g') i₁) (Y :=
      pullback (X := pullback f' g') (pullback.snd f' g') i₂) (pullback.fst (pullback.fst f' g') i₁)
      (pullback.fst (pullback.snd f' g') i₂))
left : (pullback.fst (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂)) t = T.x
ht₂ : (pullback.snd (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂)) t = T.y
⊢ (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) ((Iso.hom (pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂)) t : ↥(pullback f g)) =
    z
have h : (pullback.snd (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂) ≫
      pullback.fst (pullback.snd f' g') i₂)
    t =
  z
Tactic: rw [pullback_map_eq_pullbackFstFstIso_inv, ← Scheme.Hom.comp_apply, Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
P : MorphismProperty Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
h : HasPullback f g
hg : P g
x : ↥X
y : ↥Y
hxy : Eq (α := ↥S) (f x : ↥S) (g y : ↥S)
⊢ ∃ (a : ↥(pullback f g)), (pullback.fst f g) a = x
have obtain : ∀ (a : ↥(pullback f g)) (b : (pullback.fst f g) a = x) (h_1 : (pullback.snd f g) a = y),
  ∃ (a : ↥(pullback f g)), (pullback.fst f g) a = x
Tactic: obtain ⟨a, b, h⟩ := Pullback.exists_preimage_pullback x y hxy
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ Function.Surjective (α := (fun (X : Type u) ↦ X) (forget.obj (pullback f g))) (β :=
    (fun (X : Type u) ↦ X) (pullback (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)))
have refine : ∀ (x : (fun (X : Type u) ↦ X) (Types.PullbackObj (forget.map f) (forget.map g))),
  ∃ (a : (fun (X : Type u) ↦ X) (forget.obj (pullback f g))),
    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)))
        a =
      x
Tactic: refine .of_comp_left (fun x ↦ ?_) <|
    injective_of_mono (Types.pullbackIsoPullback (forget.map f) (forget.map g)).hom
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
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))
⊢ ∃ (a : (fun (X : Type u) ↦ X) (forget.obj (pullback f g))),
    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)))
        a =
      x
have obtain : ∀ (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),
  ∃ (a : (fun (X : Type u) ↦ X) (forget.obj (pullback f g))),
    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)))
        a =
      x
Tactic: obtain ⟨z, h1, h2⟩ := Pullback.exists_preimage_pullback (f := f) (g := g) x.1.1 x.1.2 x.2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
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
⊢ ∃ (a : (fun (X : Type u) ↦ X) (forget.obj (pullback f g))),
    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)))
        a =
      x
have 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 =
  x
Tactic: use z
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
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
⊢ 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
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PullbackCarrier (goal)
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
⊢ 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
have 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
Tactic: ext