-- Mathlib/AlgebraicGeometry/PullbackCarrier.lean
lemma Triplet.Spec_ofPointTensor_SpecTensorTo (T : Triplet f g) (p : Spec T.tensor) :
    Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      Spec.map (ofPointTensor (T.SpecTensorTo.base p)) ≫
      Spec.map (tensorCongr (T.ofPoint_SpecTensorTo p).symm).hom =
    (Spec T.tensor).fromSpecResidueField p

Proof state:
case h₀
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↑↑(Spec T.tensor).toPresheafedSpace
⊢ ((Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
          Spec.map (ofPointTensor ((ConcreteCategory.hom T.SpecTensorTo.base) 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]

Result:
case h₀
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↑↑(Spec T.tensor).toPresheafedSpace
⊢ Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      Spec.map (ofPointTensor ((ConcreteCategory.hom T.SpecTensorTo.base) p)) ≫
        (ofPoint ((ConcreteCategory.hom T.SpecTensorTo.base) p)).SpecTensorTo ≫ pullback.fst f g =
    (Spec T.tensor).fromSpecResidueField p ≫ T.SpecTensorTo ≫ pullback.fst f g

Proof state:
case h₀
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↑↑(Spec T.tensor).toPresheafedSpace
⊢ (Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
        Spec.map (ofPointTensor ((ConcreteCategory.hom T.SpecTensorTo.base) 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]

Result:
case h₀
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↑↑(Spec T.tensor).toPresheafedSpace
⊢ ((Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
          Spec.map (ofPointTensor ((ConcreteCategory.hom T.SpecTensorTo.base) 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

Proof state:
case h₀
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↑↑(Spec T.tensor).toPresheafedSpace
⊢ Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      Spec.map (ofPointTensor ((ConcreteCategory.hom T.SpecTensorTo.base) p)) ≫
        (ofPoint ((ConcreteCategory.hom T.SpecTensorTo.base) p)).SpecTensorTo ≫ pullback.fst f g =
    (Spec T.tensor).fromSpecResidueField p ≫ T.SpecTensorTo ≫ pullback.fst f g

Tactic:
rw [← Hom.Spec_map_residueFieldMap_fromSpecResidueField_assoc, ofPointTensor_SpecTensorTo_assoc]

Result:
no goals

Proof state:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↑↑(Spec T.tensor).toPresheafedSpace
⊢ Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      Spec.map (ofPointTensor ((ConcreteCategory.hom T.SpecTensorTo.base) p)) ≫ Spec.map (tensorCongr ⋯).hom =
    (Spec T.tensor).fromSpecResidueField p

Tactic:
apply T.Spec_map_tensor_isPullback.hom_ext

Result:
case h₀
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↑↑(Spec T.tensor).toPresheafedSpace
⊢ (Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
        Spec.map (ofPointTensor ((ConcreteCategory.hom T.SpecTensorTo.base) p)) ≫ Spec.map (tensorCongr ⋯).hom) ≫
      Spec.map T.tensorInl =
    (Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInl

case h₁
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↑↑(Spec T.tensor).toPresheafedSpace
⊢ (Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
        Spec.map (ofPointTensor ((ConcreteCategory.hom T.SpecTensorTo.base) p)) ≫ Spec.map (tensorCongr ⋯).hom) ≫
      Spec.map T.tensorInr =
    (Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInr

Proof state:
case h₁
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↑↑(Spec T.tensor).toPresheafedSpace
⊢ ((Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
          Spec.map (ofPointTensor ((ConcreteCategory.hom T.SpecTensorTo.base) 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]

Result:
case h₁
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↑↑(Spec T.tensor).toPresheafedSpace
⊢ Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      Spec.map (ofPointTensor ((ConcreteCategory.hom T.SpecTensorTo.base) p)) ≫
        (ofPoint ((ConcreteCategory.hom T.SpecTensorTo.base) p)).SpecTensorTo ≫ pullback.snd f g =
    (Spec T.tensor).fromSpecResidueField p ≫ T.SpecTensorTo ≫ pullback.snd f g

Proof state:
case h₁
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↑↑(Spec T.tensor).toPresheafedSpace
⊢ (Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
        Spec.map (ofPointTensor ((ConcreteCategory.hom T.SpecTensorTo.base) 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]

Result:
case h₁
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↑↑(Spec T.tensor).toPresheafedSpace
⊢ ((Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
          Spec.map (ofPointTensor ((ConcreteCategory.hom T.SpecTensorTo.base) 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

Proof state:
case h₁
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↑↑(Spec T.tensor).toPresheafedSpace
⊢ Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      Spec.map (ofPointTensor ((ConcreteCategory.hom T.SpecTensorTo.base) p)) ≫
        (ofPoint ((ConcreteCategory.hom T.SpecTensorTo.base) p)).SpecTensorTo ≫ pullback.snd f g =
    (Spec T.tensor).fromSpecResidueField p ≫ T.SpecTensorTo ≫ pullback.snd f g

Tactic:
rw [← Hom.Spec_map_residueFieldMap_fromSpecResidueField_assoc, ofPointTensor_SpecTensorTo_assoc]

Result:
no goals