Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: case h₀
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
⊢ pullback.fst (pullback.snd (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R S))))
        (pullback.snd (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R S)))) ≫
      pullback.fst (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R S))) =
    Over.Hom.left
        (Hom.asOver
            ((pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))).hom ≫
              (pullbackSpecIso' R S T).hom)
            (Spec (of S)) ⊗ₘ
          Hom.asOver
            ((pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))).hom ≫
              (pullbackSpecIso' R S T).hom)
            (Spec (of S))) ≫
      (pullbackSpecIso S (S ⊗[R] T) (S ⊗[R] T)).hom ≫
        Spec.map (ofHom (mapRingHom (algebraMap R S) ↑includeRight ↑includeRight ⋯ ⋯)) ≫
          Spec.map (ofHom includeLeftRingHom)

pp: case h₁
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
⊢ pullback.snd (pullback.snd (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R S))))
        (pullback.snd (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R S)))) ≫
      pullback.fst (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R S))) =
    Over.Hom.left
        (Hom.asOver
            ((pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))).hom ≫
              (pullbackSpecIso' R S T).hom)
            (Spec (of S)) ⊗ₘ
          Hom.asOver
            ((pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))).hom ≫
              (pullbackSpecIso' R S T).hom)
            (Spec (of S))) ≫
      (pullbackSpecIso S (S ⊗[R] T) (S ⊗[R] T)).hom ≫
        Spec.map (ofHom (mapRingHom (algebraMap R S) ↑includeRight ↑includeRight ⋯ ⋯)) ≫ Spec.map (ofHom ↑includeRight)

Tactic:
· simp only [← Spec.map_comp, ← CommRingCat.ofHom_comp,
      Algebra.TensorProduct.mapRingHom_comp_includeLeftRingHom]
    simp [specOverSpec_over]
    erw [Over.tensorHom_left_fst_assoc]
    simp [pullbackSpecIso']
    rfl

Goal state after:
case h₁
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
⊢ pullback.snd (pullback.snd (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R S))))
        (pullback.snd (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R S)))) ≫
      pullback.fst (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R S))) =
    Over.Hom.left
        (Hom.asOver
            ((pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))).hom ≫
              (pullbackSpecIso' R S T).hom)
            (Spec (of S)) ⊗ₘ
          Hom.asOver
            ((pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))).hom ≫
              (pullbackSpecIso' R S T).hom)
            (Spec (of S))) ≫
      (pullbackSpecIso S (S ⊗[R] T) (S ⊗[R] T)).hom ≫
        Spec.map (ofHom (mapRingHom (algebraMap R S) ↑includeRight ↑includeRight ⋯ ⋯)) ≫ Spec.map (ofHom ↑includeRight)