awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↥(pullback f g)
⊢ ((residueFieldCongr ⋯).inv ≫ Hom.residueFieldMap f (Triplet.ofPoint t).x) ≫ Hom.residueFieldMap (pullback.fst f g) t =
    ((residueFieldCongr ⋯).inv ≫ Hom.residueFieldMap g (Triplet.ofPoint t).y) ≫ Hom.residueFieldMap (pullback.snd f g) t

Tactic:
simp [← residueFieldMap_comp, Scheme.Hom.residueFieldMap_congr pullback.condition]

Premises used: AlgebraicGeometry.Scheme.Hom.residueFieldMap_congr, CategoryTheory.Limits.pullback.condition, AlgebraicGeometry.Scheme.residueFieldMap_comp
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↥(pullback f g)
h₀ :
  (Spec.map (ofPointTensor t) ≫ (Triplet.ofPoint t).SpecTensorTo) ≫ pullback.fst f g =
    (pullback f g).fromSpecResidueField t ≫ pullback.fst f g
h₁ :
  (Spec.map (ofPointTensor t) ≫ (Triplet.ofPoint t).SpecTensorTo) ≫ pullback.snd f g =
    (pullback f g).fromSpecResidueField t ≫ pullback.snd f g
⊢ Spec.map (ofPointTensor t) ≫ (Triplet.ofPoint t).SpecTensorTo = (pullback f g).fromSpecResidueField t

Tactic:
apply pullback.hom_ext

Premises used: CategoryTheory.Limits.pullback.hom_ext
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↥(pullback f g)
h₀ :
  (Spec.map (ofPointTensor t) ≫ (Triplet.ofPoint t).SpecTensorTo) ≫ pullback.fst f g =
    CategoryStruct.comp (Y := Spec (X.residueField ((pullback.fst f g) t)))
      (Spec.map (Hom.residueFieldMap (pullback.fst f g) t)) (X.fromSpecResidueField ((pullback.fst f g) t))
⊢ (Spec.map (ofPointTensor t) ≫ (Triplet.ofPoint t).SpecTensorTo) ≫ pullback.fst f g =
    (pullback f g).fromSpecResidueField t ≫ pullback.fst f g

Tactic:
rw [← Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField]

Premises used: AlgebraicGeometry.Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↥(pullback f g)
h₀ :
  Spec.map (ofPointTensor t) ≫ Spec.map (Triplet.ofPoint t).tensorInl ≫ X.fromSpecResidueField ((pullback.fst f g) t) =
    CategoryStruct.comp (Y := Spec (X.residueField ((pullback.fst f g) t)))
      (Spec.map (Hom.residueFieldMap (pullback.fst f g) t)) (X.fromSpecResidueField ((pullback.fst f g) t))
⊢ (Spec.map (ofPointTensor t) ≫ (Triplet.ofPoint t).SpecTensorTo) ≫ pullback.fst f g =
    CategoryStruct.comp (Y := Spec (X.residueField ((pullback.fst f g) t)))
      (Spec.map (Hom.residueFieldMap (pullback.fst f g) t)) (X.fromSpecResidueField ((pullback.fst f g) t))

Tactic:
simp only [Category.assoc, Triplet.specTensorTo_fst, Triplet.ofPoint_x]

Premises used: AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_fst, CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_x
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↥(pullback f g)
h₀ :
  Spec.map (ofPointTensor t) ≫ Spec.map (Triplet.ofPoint t).tensorInl ≫ X.fromSpecResidueField ((pullback.fst f g) t) =
    CategoryStruct.comp (Y :=
        Spec
          (pushout ((residueFieldCongr ⋯).inv ≫ Hom.residueFieldMap f (Triplet.ofPoint t).x)
            ((residueFieldCongr ⋯).inv ≫ Hom.residueFieldMap g (Triplet.ofPoint t).y)))
        (Spec.map
          (pushout.desc (Hom.residueFieldMap (pullback.fst f g) t) (Hom.residueFieldMap (pullback.snd f g) t) ⋯))
        (Spec.map
          (pushout.inl ((residueFieldCongr ⋯).inv ≫ Hom.residueFieldMap f (Triplet.ofPoint t).x)
            ((residueFieldCongr ⋯).inv ≫ Hom.residueFieldMap g (Triplet.ofPoint t).y))) ≫
      X.fromSpecResidueField ((pullback.fst f g) t)
⊢ Spec.map (ofPointTensor t) ≫ Spec.map (Triplet.ofPoint t).tensorInl ≫ X.fromSpecResidueField ((pullback.fst f g) t) =
    CategoryStruct.comp (Y := Spec (X.residueField ((pullback.fst f g) t)))
      (Spec.map (Hom.residueFieldMap (pullback.fst f g) t)) (X.fromSpecResidueField ((pullback.fst f g) t))

Tactic:
rw [← pushout.inl_desc _ _ (residueFieldCongr_inv_residueFieldMap_ofPoint t), Spec.map_comp]

Premises used: AlgebraicGeometry.Scheme.Pullback.residueFieldCongr_inv_residueFieldMap_ofPoint, AlgebraicGeometry.Spec.map_comp, CategoryTheory.Limits.pushout.inl_desc
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↥(pullback f g)
⊢ Spec.map (ofPointTensor t) ≫ Spec.map (Triplet.ofPoint t).tensorInl ≫ X.fromSpecResidueField ((pullback.fst f g) t) =
    CategoryStruct.comp (Y :=
        Spec
          (pushout ((residueFieldCongr ⋯).inv ≫ Hom.residueFieldMap f (Triplet.ofPoint t).x)
            ((residueFieldCongr ⋯).inv ≫ Hom.residueFieldMap g (Triplet.ofPoint t).y)))
        (Spec.map
          (pushout.desc (Hom.residueFieldMap (pullback.fst f g) t) (Hom.residueFieldMap (pullback.snd f g) t) ⋯))
        (Spec.map
          (pushout.inl ((residueFieldCongr ⋯).inv ≫ Hom.residueFieldMap f (Triplet.ofPoint t).x)
            ((residueFieldCongr ⋯).inv ≫ Hom.residueFieldMap g (Triplet.ofPoint t).y))) ≫
      X.fromSpecResidueField ((pullback.fst f g) t)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↥(pullback f g)
h₁ :
  (Spec.map (ofPointTensor t) ≫ (Triplet.ofPoint t).SpecTensorTo) ≫ pullback.snd f g =
    CategoryStruct.comp (Y := Spec (Y.residueField ((pullback.snd f g) t)))
      (Spec.map (Hom.residueFieldMap (pullback.snd f g) t)) (Y.fromSpecResidueField ((pullback.snd f g) t))
⊢ (Spec.map (ofPointTensor t) ≫ (Triplet.ofPoint t).SpecTensorTo) ≫ pullback.snd f g =
    (pullback f g).fromSpecResidueField t ≫ pullback.snd f g

Tactic:
rw [← Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField]

Premises used: AlgebraicGeometry.Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↥(pullback f g)
h₁ :
  Spec.map (ofPointTensor t) ≫ Spec.map (Triplet.ofPoint t).tensorInr ≫ Y.fromSpecResidueField ((pullback.snd f g) t) =
    CategoryStruct.comp (Y := Spec (Y.residueField ((pullback.snd f g) t)))
      (Spec.map (Hom.residueFieldMap (pullback.snd f g) t)) (Y.fromSpecResidueField ((pullback.snd f g) t))
⊢ (Spec.map (ofPointTensor t) ≫ (Triplet.ofPoint t).SpecTensorTo) ≫ pullback.snd f g =
    CategoryStruct.comp (Y := Spec (Y.residueField ((pullback.snd f g) t)))
      (Spec.map (Hom.residueFieldMap (pullback.snd f g) t)) (Y.fromSpecResidueField ((pullback.snd f g) t))

Tactic:
simp only [Category.assoc, Triplet.specTensorTo_snd, Triplet.ofPoint_y]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_snd, AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_y
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↥(pullback f g)
h₁ :
  Spec.map (ofPointTensor t) ≫ Spec.map (Triplet.ofPoint t).tensorInr ≫ Y.fromSpecResidueField ((pullback.snd f g) t) =
    CategoryStruct.comp (Y :=
        Spec
          (pushout ((residueFieldCongr ⋯).inv ≫ Hom.residueFieldMap f (Triplet.ofPoint t).x)
            ((residueFieldCongr ⋯).inv ≫ Hom.residueFieldMap g (Triplet.ofPoint t).y)))
        (Spec.map
          (pushout.desc (Hom.residueFieldMap (pullback.fst f g) t) (Hom.residueFieldMap (pullback.snd f g) t) ⋯))
        (Spec.map
          (pushout.inr ((residueFieldCongr ⋯).inv ≫ Hom.residueFieldMap f (Triplet.ofPoint t).x)
            ((residueFieldCongr ⋯).inv ≫ Hom.residueFieldMap g (Triplet.ofPoint t).y))) ≫
      Y.fromSpecResidueField ((pullback.snd f g) t)
⊢ Spec.map (ofPointTensor t) ≫ Spec.map (Triplet.ofPoint t).tensorInr ≫ Y.fromSpecResidueField ((pullback.snd f g) t) =
    CategoryStruct.comp (Y := Spec (Y.residueField ((pullback.snd f g) t)))
      (Spec.map (Hom.residueFieldMap (pullback.snd f g) t)) (Y.fromSpecResidueField ((pullback.snd f g) t))

Tactic:
rw [← pushout.inr_desc _ _ (residueFieldCongr_inv_residueFieldMap_ofPoint t), Spec.map_comp]

Premises used: CategoryTheory.Limits.pushout.inr_desc, AlgebraicGeometry.Scheme.Pullback.residueFieldCongr_inv_residueFieldMap_ofPoint, AlgebraicGeometry.Spec.map_comp
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↥(pullback f g)
⊢ Spec.map (ofPointTensor t) ≫ Spec.map (Triplet.ofPoint t).tensorInr ≫ Y.fromSpecResidueField ((pullback.snd f g) t) =
    CategoryStruct.comp (Y :=
        Spec
          (pushout ((residueFieldCongr ⋯).inv ≫ Hom.residueFieldMap f (Triplet.ofPoint t).x)
            ((residueFieldCongr ⋯).inv ≫ Hom.residueFieldMap g (Triplet.ofPoint t).y)))
        (Spec.map
          (pushout.desc (Hom.residueFieldMap (pullback.fst f g) t) (Hom.residueFieldMap (pullback.snd f g) t) ⋯))
        (Spec.map
          (pushout.inr ((residueFieldCongr ⋯).inv ≫ Hom.residueFieldMap f (Triplet.ofPoint t).x)
            ((residueFieldCongr ⋯).inv ≫ Hom.residueFieldMap g (Triplet.ofPoint t).y))) ≫
      Y.fromSpecResidueField ((pullback.snd f g) t)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↥(pullback f g)
⊢ (Triplet.ofPoint t).SpecTensorTo (SpecOfPoint t) = t

Tactic:
simp [SpecOfPoint, ← Scheme.Hom.comp_apply, ofPointTensor_SpecTensorTo]

Premises used: AlgebraicGeometry.Scheme.Pullback.SpecOfPoint, AlgebraicGeometry.Scheme.Hom.comp_apply, AlgebraicGeometry.Scheme.Pullback.ofPointTensor_SpecTensorTo
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T T' : Triplet f g
h : T = T'
subst : Spec.map (Triplet.tensorCongr ⋯).hom ≫ T.SpecTensorTo = T.SpecTensorTo
⊢ Spec.map (Triplet.tensorCongr h).hom ≫ T.SpecTensorTo = T'.SpecTensorTo

Tactic:
subst h
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
⊢ Spec.map (Triplet.tensorCongr ⋯).hom ≫ T.SpecTensorTo = T.SpecTensorTo

Tactic:
simp only [Triplet.tensorCongr_refl, Iso.refl_hom, Spec.map_id, Category.id_comp]

Premises used: AlgebraicGeometry.Spec.map_id, CategoryTheory.Iso.refl_hom, AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr_refl, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
h₀ :
  (Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
        Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ Spec.map (tensorCongr ⋯).hom) ≫
      Spec.map T.tensorInl =
    (Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInl
h₁ :
  (Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
        Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ Spec.map (tensorCongr ⋯).hom) ≫
      Spec.map T.tensorInr =
    (Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInr
⊢ Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ Spec.map (tensorCongr ⋯).hom =
    (Spec T.tensor).fromSpecResidueField p

Tactic:
apply T.isPullback_SpecMap_tensor.hom_ext

Premises used: CategoryTheory.IsPullback.hom_ext, AlgebraicGeometry.Scheme.Pullback.Triplet.isPullback_SpecMap_tensor
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
h₀ :
  ((Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
          Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ Spec.map (tensorCongr ⋯).hom) ≫
        Spec.map T.tensorInl) ≫
      X.fromSpecResidueField T.x =
    ((Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInl) ≫ X.fromSpecResidueField T.x
⊢ (Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
        Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ Spec.map (tensorCongr ⋯).hom) ≫
      Spec.map T.tensorInl =
    (Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInl

Tactic:
rw [← cancel_mono <| X.fromSpecResidueField T.x]

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.Pullback.Triplet.x, AlgebraicGeometry.Scheme.fromSpecResidueField
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
h₀ :
  Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ SpecTensorTo (ofPoint (T.SpecTensorTo p)) ≫ pullback.fst f g =
    (Spec T.tensor).fromSpecResidueField p ≫ T.SpecTensorTo ≫ pullback.fst f g
⊢ ((Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
          Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ Spec.map (tensorCongr ⋯).hom) ≫
        Spec.map T.tensorInl) ≫
      X.fromSpecResidueField T.x =
    ((Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInl) ≫ X.fromSpecResidueField T.x

Tactic:
simp_rw [Category.assoc, ← T.specTensorTo_fst, tensorCongr_SpecTensorTo_assoc]

Premises used: AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_fst, CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Pullback.tensorCongr_SpecTensorTo_assoc
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
h₀ :
  Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ SpecTensorTo (ofPoint (T.SpecTensorTo p)) ≫ pullback.fst f g =
    Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      (pullback f g).fromSpecResidueField (T.SpecTensorTo p) ≫ pullback.fst f g
h₁ h₂ :
  Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      (pullback f g).fromSpecResidueField (T.SpecTensorTo p) ≫ pullback.fst f g =
    Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      (pullback f g).fromSpecResidueField (T.SpecTensorTo p) ≫ pullback.fst f g
⊢ Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ SpecTensorTo (ofPoint (T.SpecTensorTo p)) ≫ pullback.fst f g =
    (Spec T.tensor).fromSpecResidueField p ≫ T.SpecTensorTo ≫ pullback.fst f g

Tactic:
rw [← Hom.SpecMap_residueFieldMap_fromSpecResidueField_assoc, ofPointTensor_SpecTensorTo_assoc]

Premises used: AlgebraicGeometry.Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField_assoc, AlgebraicGeometry.Scheme.Pullback.ofPointTensor_SpecTensorTo_assoc
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
h₁ :
  ((Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
          Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ Spec.map (tensorCongr ⋯).hom) ≫
        Spec.map T.tensorInr) ≫
      Y.fromSpecResidueField T.y =
    ((Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInr) ≫ Y.fromSpecResidueField T.y
⊢ (Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
        Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ Spec.map (tensorCongr ⋯).hom) ≫
      Spec.map T.tensorInr =
    (Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInr

Tactic:
rw [← cancel_mono <| Y.fromSpecResidueField T.y]

Premises used: AlgebraicGeometry.Scheme.Pullback.Triplet.y, CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.fromSpecResidueField
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
h₁ :
  Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ SpecTensorTo (ofPoint (T.SpecTensorTo p)) ≫ pullback.snd f g =
    (Spec T.tensor).fromSpecResidueField p ≫ T.SpecTensorTo ≫ pullback.snd f g
⊢ ((Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
          Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ Spec.map (tensorCongr ⋯).hom) ≫
        Spec.map T.tensorInr) ≫
      Y.fromSpecResidueField T.y =
    ((Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInr) ≫ Y.fromSpecResidueField T.y

Tactic:
simp_rw [Category.assoc, ← T.specTensorTo_snd, tensorCongr_SpecTensorTo_assoc]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_snd, AlgebraicGeometry.Scheme.Pullback.tensorCongr_SpecTensorTo_assoc
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
h₁ :
  Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ SpecTensorTo (ofPoint (T.SpecTensorTo p)) ≫ pullback.snd f g =
    Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      (pullback f g).fromSpecResidueField (T.SpecTensorTo p) ≫ pullback.snd f g
h₂ h₃ :
  Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      (pullback f g).fromSpecResidueField (T.SpecTensorTo p) ≫ pullback.snd f g =
    Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      (pullback f g).fromSpecResidueField (T.SpecTensorTo p) ≫ pullback.snd f g
⊢ Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ SpecTensorTo (ofPoint (T.SpecTensorTo p)) ≫ pullback.snd f g =
    (Spec T.tensor).fromSpecResidueField p ≫ T.SpecTensorTo ≫ pullback.snd f g

Tactic:
rw [← Hom.SpecMap_residueFieldMap_fromSpecResidueField_assoc, ofPointTensor_SpecTensorTo_assoc]

Premises used: AlgebraicGeometry.Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField_assoc, AlgebraicGeometry.Scheme.Pullback.ofPointTensor_SpecTensorTo_assoc
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
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))
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₂
⊢ 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
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
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))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T₁ T₂ : (T : Triplet f g) × ↥(Spec T.tensor)
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₂
⊢ (∃ (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:
obtain ⟨T, _⟩ := T₁
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
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)
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)
⊢ (∃ (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₂
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
snd snd_1 : ↥(Spec T.tensor)
e :
  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 ⋯).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:
simpa [e]