Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
⊢ Over.Hom.left
        (LaxMonoidal.μ (Over.pullback (Spec.map (ofHom (algebraMap R S)))) (Over.mk (Spec.map (ofHom (algebraMap R T))))
          (Over.mk (Spec.map (ofHom (algebraMap R T))))) ≫
      pullback.fst
        (pullback.fst (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R T))) ≫
          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 ⋯ ⋯)) ≫ (pullbackSpecIso R T T).inv

Tactic:
ext

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
⊢ (Over.Hom.left
          (LaxMonoidal.μ (Over.pullback (Spec.map (ofHom (algebraMap R S))))
            (Over.mk (Spec.map (ofHom (algebraMap R T)))) (Over.mk (Spec.map (ofHom (algebraMap R T))))) ≫
        pullback.fst
          (pullback.fst (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R T))) ≫
            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 T))) =
    (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 ⋯ ⋯)) ≫
            (pullbackSpecIso R T T).inv) ≫
      pullback.fst (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R T)))

case h₁
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
⊢ (Over.Hom.left
          (LaxMonoidal.μ (Over.pullback (Spec.map (ofHom (algebraMap R S))))
            (Over.mk (Spec.map (ofHom (algebraMap R T)))) (Over.mk (Spec.map (ofHom (algebraMap R T))))) ≫
        pullback.fst
          (pullback.fst (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R T))) ≫
            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 T))) =
    (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 ⋯ ⋯)) ≫
            (pullbackSpecIso R T T).inv) ≫
      pullback.snd (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R T)))