awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  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')
⊢ 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:
use pullback.fst f g t

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.Limits.pullback.fst, AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe
-- 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 :
  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')
⊢ 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:
rw [← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply
-- 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)
⊢ 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:
simp
-- 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 :
  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')
⊢ 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:
use pullback.snd f g t

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.pullback.snd, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe
-- 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 :
  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')
⊢ 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:
rw [← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply
-- 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)
⊢ 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:
simp
-- 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')
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 ⋯
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
⊢ 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

Premises used: AlgebraicGeometry.Scheme.Pullback.Triplet.exists_preimage
-- 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')
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 ⋯
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
⊢ 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

Premises used: AlgebraicGeometry.Scheme.Pullback.Triplet.exists_preimage
-- 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')
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
⊢ Eq (α := ↥(pullback f' g')) ((pullback.fst (pullback.fst f' g') i₁) w₁ : ↥(pullback f' g'))
    ((pullback.fst (pullback.snd f' g') i₂) w₂ : ↥(pullback f' g'))

Tactic:
simp [hw₁.left, hw₂.left, T₁, T₂]

Premises used: And.left
-- 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')
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₂ ⋯
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
⊢ 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

Premises used: AlgebraicGeometry.Scheme.Pullback.t, AlgebraicGeometry.Scheme.Pullback.Triplet.exists_preimage
-- 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')
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
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
⊢ Membership.mem (γ := Set ↥(pullback f' g'))
    (Set.range (ι := ↥(pullback f g)) ⇑(pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂)) z

Tactic:
use (pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).hom t

Premises used: CategoryTheory.Limits.pullbackFstFstIso, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, CategoryTheory.Iso.hom, DFunLike.coe
-- 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')
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
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
⊢ (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:
rw [pullback_map_eq_pullbackFstFstIso_inv, ← Scheme.Hom.comp_apply, Iso.hom_inv_id_assoc]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.Limits.pullback_map_eq_pullbackFstFstIso_inv
-- 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')
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.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:
simp [ht₂, T, hw₂.left, T₂]

Premises used: And.left
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
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)
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
⊢ ∃ (a : ↥(pullback f g)), (pullback.fst f g) a = x

Tactic:
obtain ⟨a, b, h⟩ := Pullback.exists_preimage_pullback x y hxy

Premises used: AlgebraicGeometry.Scheme.Pullback.exists_preimage_pullback
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
P : MorphismProperty Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
h_1 : HasPullback f g
hg : P g
x : ↥X
y : ↥Y
hxy : Eq (α := ↥S) (f x : ↥S) (g y : ↥S)
a : ↥(pullback f g)
b : (pullback.fst f g) a = x
h : (pullback.snd f g) a = y
w : ↥(pullback f g)
h₁ : (pullback.fst f g) a = x
⊢ ∃ (a : ↥(pullback f g)), (pullback.fst f g) a = x

Tactic:
use a
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
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)))

Tactic:
.of_comp_left (fun x ↦ ?_) <|
    injective_of_mono (Types.pullbackIsoPullback (forget.map f) (forget.map g)).hom

Premises used: AlgebraicGeometry.Scheme.forget, Function.Surjective.of_comp_left, CategoryTheory.Limits.Types.pullbackIsoPullback, CategoryTheory.Functor.map, CategoryTheory.injective_of_mono, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
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
⊢ 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)))

Tactic:
refine .of_comp_left (fun x ↦ ?_) <|
    injective_of_mono (Types.pullbackIsoPullback (forget.map f) (forget.map g)).hom

Premises used: AlgebraicGeometry.Scheme.forget, CategoryTheory.Limits.Types.pullbackIsoPullback, CategoryTheory.Functor.map, CategoryTheory.injective_of_mono, CategoryTheory.Iso.hom
-- 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))
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
⊢ ∃ (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

Premises used: Prod.fst, Subtype.val, Prod.snd, AlgebraicGeometry.Scheme.Pullback.exists_preimage_pullback, Subtype.property
-- 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 =
    x
⊢ ∃ (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:
use z