-- 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)
⊢ ∃ (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))
have 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 sorry).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