Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: case e'_2
R✝¹ R✝ A : CommRingCat
X M G : Scheme
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Bialgebra R T
e_1✝ :
  ((OverClass.asOver (pullback (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))) (Spec (of S)) ⊗
          OverClass.asOver (pullback (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))) (Spec (of S))).left ⟶
      Spec (of T)) =
    (((Over.pullback (Spec.map (ofHom (algebraMap R S)))).obj (Over.mk (Spec.map (ofHom (algebraMap R T)))) ⊗
          (Over.pullback (Spec.map (ofHom (algebraMap R S)))).obj (Over.mk (Spec.map (ofHom (algebraMap R T))))).left ⟶
      Spec (of T))
⊢ (Over.Hom.left
          (μ ≫
            Hom.asOver
              (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) ≪≫ pullbackSpecIso' R S T).hom
              (Spec (of S))) ≫
        (pullbackSpecIso' R S T).inv) ≫
      pullback.snd (Spec (of S) ↘ Spec (of R)) (Spec (of T) ↘ Spec (of R)) =
    (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 (Over.mk (Spec.map (ofHom (algebraMap R T))) ⊗ Over.mk (Spec.map (ofHom (algebraMap R T)))).hom
          (Spec.map (ofHom (algebraMap R S)))) ≫
      (pullbackSpecIso R T T).hom ≫ Spec.map (ofHom (Bialgebra.comulAlgHom R T).toRingHom)

pp: case e'_3
R✝¹ R✝ A : CommRingCat
X M G : Scheme
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Bialgebra R T
e_1✝ :
  ((OverClass.asOver (pullback (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))) (Spec (of S)) ⊗
          OverClass.asOver (pullback (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))) (Spec (of S))).left ⟶
      Spec (of T)) =
    (((Over.pullback (Spec.map (ofHom (algebraMap R S)))).obj (Over.mk (Spec.map (ofHom (algebraMap R T)))) ⊗
          (Over.pullback (Spec.map (ofHom (algebraMap R S)))).obj (Over.mk (Spec.map (ofHom (algebraMap R T))))).left ⟶
      Spec (of T))
⊢ (Over.Hom.left
          ((Hom.asOver
                (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) ≪≫ pullbackSpecIso' R S T).hom
                (Spec (of S)) ⊗ₘ
              Hom.asOver
                (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) ≪≫ pullbackSpecIso' R S T).hom
                (Spec (of S))) ≫
            μ) ≫
        (pullbackSpecIso' R S T).inv) ≫
      pullback.snd (Spec (of S) ↘ Spec (of R)) (Spec (of T) ↘ Spec (of R)) =
    (Over.Hom.left
          (Hom.asOver
              (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) ≪≫ pullbackSpecIso' R S T).hom
              (Spec (of S)) ⊗ₘ
            Hom.asOver
              (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) ≪≫ 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.toRingHom includeRight.toRingHom ⋯ ⋯)) ≫
            (pullbackSpecIso R T T).inv) ≫
      (pullbackSpecIso R T T).hom ≫ Spec.map (ofHom (Bialgebra.comulAlgHom R T).toRingHom)

Tactic:
· simp [Scheme.monObjAsOverPullback_mul, pullbackSpecIso', specOverSpec_over,
          OverClass.asOver, Hom.asOver, OverClass.asOverHom, mul_spec_asOver_spec_left]

Goal state after:
case e'_3
R✝¹ R✝ A : CommRingCat
X M G : Scheme
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Bialgebra R T
e_1✝ :
  ((OverClass.asOver (pullback (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))) (Spec (of S)) ⊗
          OverClass.asOver (pullback (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))) (Spec (of S))).left ⟶
      Spec (of T)) =
    (((Over.pullback (Spec.map (ofHom (algebraMap R S)))).obj (Over.mk (Spec.map (ofHom (algebraMap R T)))) ⊗
          (Over.pullback (Spec.map (ofHom (algebraMap R S)))).obj (Over.mk (Spec.map (ofHom (algebraMap R T))))).left ⟶
      Spec (of T))
⊢ (Over.Hom.left
          ((Hom.asOver
                (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) ≪≫ pullbackSpecIso' R S T).hom
                (Spec (of S)) ⊗ₘ
              Hom.asOver
                (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) ≪≫ pullbackSpecIso' R S T).hom
                (Spec (of S))) ≫
            μ) ≫
        (pullbackSpecIso' R S T).inv) ≫
      pullback.snd (Spec (of S) ↘ Spec (of R)) (Spec (of T) ↘ Spec (of R)) =
    (Over.Hom.left
          (Hom.asOver
              (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) ≪≫ pullbackSpecIso' R S T).hom
              (Spec (of S)) ⊗ₘ
            Hom.asOver
              (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) ≪≫ 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.toRingHom includeRight.toRingHom ⋯ ⋯)) ≫
            (pullbackSpecIso R T T).inv) ≫
      (pullbackSpecIso R T T).hom ≫ Spec.map (ofHom (Bialgebra.comulAlgHom R T).toRingHom)