-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
h :
  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))
⊢ ∃ (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:
use T.ofPoint_SpecTensorTo p

Premises used: AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_SpecTensorTo