-- Mathlib/AlgebraicGeometry/PullbackCarrier.lean
@[reassoc]
lemma ofPointTensor_SpecTensorTo (t : ↑(pullback f g)) :
    Spec.map (ofPointTensor t) ≫ (Triplet.ofPoint t).SpecTensorTo =
      (pullback f g).fromSpecResidueField t

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

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

Result:
case h₁
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↑↑(pullback f g).toPresheafedSpace
⊢ Spec.map (ofPointTensor t) ≫
      Spec.map (Triplet.ofPoint t).tensorInr ≫
        Y.fromSpecResidueField ((ConcreteCategory.hom (pullback.snd f g).base) t) =
    (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 ((ConcreteCategory.hom (pullback.snd f g).base) t)

Proof state:
case h₁
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↑↑(pullback f g).toPresheafedSpace
⊢ Spec.map (ofPointTensor t) ≫
      Spec.map (Triplet.ofPoint t).tensorInr ≫
        Y.fromSpecResidueField ((ConcreteCategory.hom (pullback.snd f g).base) t) =
    (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 ((ConcreteCategory.hom (pullback.snd f g).base) t)

Tactic:
rfl

Result:
no goals

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

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

Result:
case h₀
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↑↑(pullback f g).toPresheafedSpace
⊢ Spec.map (ofPointTensor t) ≫
      Spec.map (Triplet.ofPoint t).tensorInl ≫
        X.fromSpecResidueField ((ConcreteCategory.hom (pullback.fst f g).base) t) =
    (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 ((ConcreteCategory.hom (pullback.fst f g).base) t)

Proof state:
case h₁
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↑↑(pullback f g).toPresheafedSpace
⊢ (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.Spec_map_residueFieldMap_fromSpecResidueField]

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

Proof state:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↑↑(pullback f g).toPresheafedSpace
⊢ Spec.map (ofPointTensor t) ≫ (Triplet.ofPoint t).SpecTensorTo = (pullback f g).fromSpecResidueField t

Tactic:
apply pullback.hom_ext

Result:
case h₀
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↑↑(pullback f g).toPresheafedSpace
⊢ (Spec.map (ofPointTensor t) ≫ (Triplet.ofPoint t).SpecTensorTo) ≫ pullback.fst f g =
    (pullback f g).fromSpecResidueField t ≫ pullback.fst f g

case h₁
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↑↑(pullback f g).toPresheafedSpace
⊢ (Spec.map (ofPointTensor t) ≫ (Triplet.ofPoint t).SpecTensorTo) ≫ pullback.snd f g =
    (pullback f g).fromSpecResidueField t ≫ pullback.snd f g

Proof state:
case h₀
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↑↑(pullback f g).toPresheafedSpace
⊢ (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.Spec_map_residueFieldMap_fromSpecResidueField]

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

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

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

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

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

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

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

Proof state:
case h₀
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↑↑(pullback f g).toPresheafedSpace
⊢ Spec.map (ofPointTensor t) ≫
      Spec.map (Triplet.ofPoint t).tensorInl ≫
        X.fromSpecResidueField ((ConcreteCategory.hom (pullback.fst f g).base) t) =
    (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 ((ConcreteCategory.hom (pullback.fst f g).base) t)

Tactic:
rfl

Result:
no goals