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
⊢ (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)))

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
⊢ (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)))

Tactic:
<;>

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)))